import sys
import pystp

print "x,y,lambda,_x,_y,_lambda:BITVECTOR(8);"
print "at,_at:BITVECTOR(4);"

vc = pystp.Stp()
# vc.setFlags('w')
# vc.setFlags('r')
vc.push()
e19223 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19224 = vc.bvConstExprFromStr("1000")
e19225 = vc.eqExpr(e19223, e19224)
e19226 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19227 = vc.bvConstExprFromStr("00000001")
e19228 = vc.sbvGtExpr(e19226, e19227)
e19229 = vc.andExpr([e19225, e19228])
e19230 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19231 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19232 = vc.iteExpr(vc.bvBoolExtract(e19230, 0), vc.bvRightShiftExpr(1 << 0, e19231), e19231)
e19233 = vc.iteExpr(vc.bvBoolExtract(e19230, 1), vc.bvRightShiftExpr(1 << 1, e19232), e19232)
e19234 = vc.iteExpr(vc.bvBoolExtract(e19230, 2), vc.bvRightShiftExpr(1 << 2, e19233), e19233)
e19235 = vc.iteExpr(vc.sbvGeExpr(e19230, vc.bvConstExprFromInt(8,8)), vc.bvConstExprFromInt(8, 0), e19234)
e19236 = vc.bvConstExprFromStr("00000001")
e19237 = vc.eqExpr(e19235, e19236)
e19238 = vc.impliesExpr(e19229, e19237)
e19239 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19240 = vc.eqExpr(vc.bvExtract(e19239, 2, 2), vc.bvConstExprFromStr("1"))
e19241 = vc.notExpr(e19240)
e19242 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19243 = vc.eqExpr(vc.bvExtract(e19242, 7, 7), vc.bvConstExprFromStr("1"))
e19244 = vc.notExpr(e19243)
e19245 = vc.orExpr([e19241, e19244])
e19246 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19247 = vc.eqExpr(vc.bvExtract(e19246, 6, 6), vc.bvConstExprFromStr("1"))
e19248 = vc.notExpr(e19247)
e19249 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19250 = vc.eqExpr(vc.bvExtract(e19249, 7, 7), vc.bvConstExprFromStr("1"))
e19251 = vc.notExpr(e19250)
e19252 = vc.orExpr([e19248, e19251])
e19253 = vc.andExpr([e19245, e19252])
e19254 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19255 = vc.eqExpr(vc.bvExtract(e19254, 0, 0), vc.bvConstExprFromStr("1"))
e19256 = vc.notExpr(e19255)
e19257 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19258 = vc.eqExpr(vc.bvExtract(e19257, 3, 3), vc.bvConstExprFromStr("1"))
e19259 = vc.orExpr([e19256, e19258])
e19260 = vc.andExpr([e19253, e19259])
e19261 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19262 = vc.bvConstExprFromStr("00000010")
e19263 = vc.eqExpr(e19261, e19262)
e19264 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19265 = vc.bvConstExprFromStr("01100100")
e19266 = vc.eqExpr(e19264, e19265)
e19267 = vc.andExpr([e19263, e19266])
e19268 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19269 = vc.bvConstExprFromStr("00110100")
e19270 = vc.eqExpr(e19268, e19269)
e19271 = vc.andExpr([e19267, e19270])
e19272 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19273 = vc.bvConstExprFromStr("0100")
e19274 = vc.eqExpr(e19272, e19273)
e19275 = vc.andExpr([e19271, e19274])
e19276 = vc.notExpr(e19275)
e19277 = vc.andExpr([e19260, e19276])
e19278 = vc.andExpr([e19238, e19277])
e19279 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19280 = vc.bvConstExprFromStr("0001")
e19281 = vc.eqExpr(e19279, e19280)
e19282 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19283 = vc.bvConstExprFromStr("11110000")
e19284 = vc.bvAndExpr(e19282, e19283)
e19285 = vc.bvConstExprFromStr("00000000")
e19286 = vc.eqExpr(e19284, e19285)
e19287 = vc.notExpr(e19286)
e19288 = vc.andExpr([e19281, e19287])
e19289 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19290 = vc.bvConstExprFromStr("0010")
e19291 = vc.eqExpr(e19289, e19290)
e19292 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19293 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19294 = vc.bvConstExprFromStr("00000100")
e19295 = vc.bvPlusExpr(8, e19293, e19294)
e19296 = vc.eqExpr(e19292, e19295)
e19297 = vc.andExpr([e19291, e19296])
e19298 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19299 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19300 = vc.bvRightShiftExpr(4, e19299)
e19301 = vc.eqExpr(e19298, e19300)
e19302 = vc.andExpr([e19297, e19301])
e19303 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19304 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19305 = vc.eqExpr(e19303, e19304)
e19306 = vc.andExpr([e19302, e19305])
e19307 = vc.andExpr([e19288, e19306])
e19308 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19309 = vc.bvConstExprFromStr("0001")
e19310 = vc.eqExpr(e19308, e19309)
e19311 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19312 = vc.bvConstExprFromStr("11110000")
e19313 = vc.bvAndExpr(e19311, e19312)
e19314 = vc.bvConstExprFromStr("00000000")
e19315 = vc.eqExpr(e19313, e19314)
e19316 = vc.andExpr([e19310, e19315])
e19317 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19318 = vc.bvConstExprFromStr("0010")
e19319 = vc.eqExpr(e19317, e19318)
e19320 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19321 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19322 = vc.eqExpr(e19320, e19321)
e19323 = vc.andExpr([e19319, e19322])
e19324 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19325 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19326 = vc.eqExpr(e19324, e19325)
e19327 = vc.andExpr([e19323, e19326])
e19328 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19329 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19330 = vc.eqExpr(e19328, e19329)
e19331 = vc.andExpr([e19327, e19330])
e19332 = vc.andExpr([e19316, e19331])
e19333 = vc.orExpr([e19307, e19332])
e19334 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19335 = vc.bvConstExprFromStr("0010")
e19336 = vc.eqExpr(e19334, e19335)
e19337 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19338 = vc.bvConstExprFromStr("11001100")
e19339 = vc.bvAndExpr(e19337, e19338)
e19340 = vc.bvConstExprFromStr("00000000")
e19341 = vc.eqExpr(e19339, e19340)
e19342 = vc.notExpr(e19341)
e19343 = vc.andExpr([e19336, e19342])
e19344 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19345 = vc.bvConstExprFromStr("0100")
e19346 = vc.eqExpr(e19344, e19345)
e19347 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19348 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19349 = vc.bvConstExprFromStr("00000010")
e19350 = vc.bvPlusExpr(8, e19348, e19349)
e19351 = vc.eqExpr(e19347, e19350)
e19352 = vc.andExpr([e19346, e19351])
e19353 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19354 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19355 = vc.bvRightShiftExpr(2, e19354)
e19356 = vc.eqExpr(e19353, e19355)
e19357 = vc.andExpr([e19352, e19356])
e19358 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19359 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19360 = vc.eqExpr(e19358, e19359)
e19361 = vc.andExpr([e19357, e19360])
e19362 = vc.andExpr([e19343, e19361])
e19363 = vc.orExpr([e19333, e19362])
e19364 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19365 = vc.bvConstExprFromStr("0010")
e19366 = vc.eqExpr(e19364, e19365)
e19367 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19368 = vc.bvConstExprFromStr("11001100")
e19369 = vc.bvAndExpr(e19367, e19368)
e19370 = vc.bvConstExprFromStr("00000000")
e19371 = vc.eqExpr(e19369, e19370)
e19372 = vc.andExpr([e19366, e19371])
e19373 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19374 = vc.bvConstExprFromStr("0100")
e19375 = vc.eqExpr(e19373, e19374)
e19376 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19377 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19378 = vc.eqExpr(e19376, e19377)
e19379 = vc.andExpr([e19375, e19378])
e19380 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19381 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19382 = vc.eqExpr(e19380, e19381)
e19383 = vc.andExpr([e19379, e19382])
e19384 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19385 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19386 = vc.eqExpr(e19384, e19385)
e19387 = vc.andExpr([e19383, e19386])
e19388 = vc.andExpr([e19372, e19387])
e19389 = vc.orExpr([e19363, e19388])
e19390 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19391 = vc.bvConstExprFromStr("0100")
e19392 = vc.eqExpr(e19390, e19391)
e19393 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19394 = vc.bvConstExprFromStr("10101010")
e19395 = vc.bvAndExpr(e19393, e19394)
e19396 = vc.bvConstExprFromStr("00000000")
e19397 = vc.eqExpr(e19395, e19396)
e19398 = vc.notExpr(e19397)
e19399 = vc.andExpr([e19392, e19398])
e19400 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19401 = vc.bvConstExprFromStr("1000")
e19402 = vc.eqExpr(e19400, e19401)
e19403 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19404 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19405 = vc.bvConstExprFromStr("00000001")
e19406 = vc.bvPlusExpr(8, e19404, e19405)
e19407 = vc.eqExpr(e19403, e19406)
e19408 = vc.andExpr([e19402, e19407])
e19409 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19410 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19411 = vc.bvRightShiftExpr(1, e19410)
e19412 = vc.eqExpr(e19409, e19411)
e19413 = vc.andExpr([e19408, e19412])
e19414 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19415 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19416 = vc.eqExpr(e19414, e19415)
e19417 = vc.andExpr([e19413, e19416])
e19418 = vc.andExpr([e19399, e19417])
e19419 = vc.orExpr([e19389, e19418])
e19420 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19421 = vc.bvConstExprFromStr("0100")
e19422 = vc.eqExpr(e19420, e19421)
e19423 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19424 = vc.bvConstExprFromStr("10101010")
e19425 = vc.bvAndExpr(e19423, e19424)
e19426 = vc.bvConstExprFromStr("00000000")
e19427 = vc.eqExpr(e19425, e19426)
e19428 = vc.andExpr([e19422, e19427])
e19429 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19430 = vc.bvConstExprFromStr("1000")
e19431 = vc.eqExpr(e19429, e19430)
e19432 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19433 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19434 = vc.eqExpr(e19432, e19433)
e19435 = vc.andExpr([e19431, e19434])
e19436 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19437 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19438 = vc.eqExpr(e19436, e19437)
e19439 = vc.andExpr([e19435, e19438])
e19440 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19441 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19442 = vc.eqExpr(e19440, e19441)
e19443 = vc.andExpr([e19439, e19442])
e19444 = vc.andExpr([e19428, e19443])
e19445 = vc.orExpr([e19419, e19444])
e19446 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19447 = vc.bvConstExprFromStr("1000")
e19448 = vc.eqExpr(e19446, e19447)
e19449 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19450 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 4))
e19451 = vc.eqExpr(e19449, e19450)
e19452 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19453 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19454 = vc.eqExpr(e19452, e19453)
e19455 = vc.andExpr([e19451, e19454])
e19456 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19457 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19458 = vc.eqExpr(e19456, e19457)
e19459 = vc.andExpr([e19455, e19458])
e19460 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19461 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19462 = vc.eqExpr(e19460, e19461)
e19463 = vc.andExpr([e19459, e19462])
e19464 = vc.andExpr([e19448, e19463])
e19465 = vc.orExpr([e19445, e19464])
e19466 = vc.andExpr([e19278, e19465])
e19467 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19468 = vc.eqExpr(vc.bvExtract(e19467, 6, 6), vc.bvConstExprFromStr("1"))
e19469 = vc.notExpr(e19468)
e19470 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19471 = vc.eqExpr(vc.bvExtract(e19470, 6, 6), vc.bvConstExprFromStr("1"))
e19472 = vc.notExpr(e19471)
e19473 = vc.notExpr(e19472)
e19474 = vc.andExpr([e19469, e19473])
e19475 = vc.andExpr([e19466, e19474])
vc.assertFormula(e19475)
vc.printAsserts()
e19476 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19477 = vc.eqExpr(vc.bvExtract(e19476, 3, 3), vc.bvConstExprFromStr("1"))
e19478 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19479 = vc.eqExpr(vc.bvExtract(e19478, 4, 4), vc.bvConstExprFromStr("1"))
e19480 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19481 = vc.eqExpr(vc.bvExtract(e19480, 5, 5), vc.bvConstExprFromStr("1"))
e19482 = vc.notExpr(e19481)
e19483 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19484 = vc.eqExpr(vc.bvExtract(e19483, 7, 7), vc.bvConstExprFromStr("1"))
e19485 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19486 = vc.eqExpr(vc.bvExtract(e19485, 0, 0), vc.bvConstExprFromStr("1"))
e19487 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19488 = vc.eqExpr(vc.bvExtract(e19487, 1, 1), vc.bvConstExprFromStr("1"))
e19489 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19490 = vc.eqExpr(vc.bvExtract(e19489, 2, 2), vc.bvConstExprFromStr("1"))
e19491 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19492 = vc.eqExpr(vc.bvExtract(e19491, 3, 3), vc.bvConstExprFromStr("1"))
e19493 = vc.notExpr(e19492)
e19494 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19495 = vc.eqExpr(vc.bvExtract(e19494, 4, 4), vc.bvConstExprFromStr("1"))
e19496 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19497 = vc.eqExpr(vc.bvExtract(e19496, 5, 5), vc.bvConstExprFromStr("1"))
e19498 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19499 = vc.eqExpr(vc.bvExtract(e19498, 6, 6), vc.bvConstExprFromStr("1"))
e19500 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e19501 = vc.eqExpr(vc.bvExtract(e19500, 7, 7), vc.bvConstExprFromStr("1"))
e19502 = vc.orExpr([e19499, e19501])
e19503 = vc.orExpr([e19497, e19502])
e19504 = vc.orExpr([e19495, e19503])
e19505 = vc.orExpr([e19493, e19504])
e19506 = vc.orExpr([e19490, e19505])
e19507 = vc.orExpr([e19488, e19506])
e19508 = vc.orExpr([e19486, e19507])
e19509 = vc.orExpr([e19484, e19508])
e19510 = vc.orExpr([e19482, e19509])
e19511 = vc.orExpr([e19479, e19510])
e19512 = vc.orExpr([e19477, e19511])
vc.push()
print "QUERY(%s);" % e19512
vc.query(e19512)

